/*
 * Traductor.c
 *
 *  Created on: Jun 20, 2009
 *      Author: gianpaolo
 */
#include "Traductor.h"

/*
 * Una casilla debe contener alguno de los 9 numeros
 */
void reglaGeneral(OutPut* cnf, int* l, int* tail) {
	int i,j, k,var;
	Clausula *clausulas = cnf->claus;

	for(i = 1; i <= 9; i++) {
		for(j = 1; j <= 9; j++) {
			clausulas[*l].numVariables = 9;
			clausulas[*l].indices = malloc(sizeof(ParOrdenado)*9);
			for(k = 1; k <= 9; k++) {
				var = (i-1)*81+(j-1)*9+(k-1);
				clausulas[*l].indices[k-1].pos = var;
				clausulas[*l].indices[k-1].bool = 1;
			}
			(*l)++;
		}
	}
}

/*
 * Una celda no puede tener dos numeros distintos
 */
void reglaCasillas(OutPut* cnf, int* l, int* tail) {
	int i,j,k,m,var;
	Clausula *clausulas = cnf->claus;
	for(i = 1; i <= 9 ; i++)
		for(j = 1; j <= 9; j++)
			for(k = 1; k <= 9; k++)
				for(m = k + 1; m <= 9; m++) {
					 var = (i-1)*81+(j-1)*9;
					 //printf("l es igual a %d\n", l);
					 clausulas[*l].numVariables = 2;
					 clausulas[*l].indices = malloc(sizeof(ParOrdenado)*2);
					 clausulas[*l].indices[0].pos = var + (k-1);
					 clausulas[*l].indices[1].pos = var + (m-1);
					 clausulas[*l].indices[1].bool = 0;
					 clausulas[*l].indices[1].bool = 0;
					 (*l)++;
				}
}

/*
 * Dos casillas distintas en una misma fila no pueden contener el mismo numero
 */
void reglaFilas(OutPut* cnf, int* l, int* tail) {
	int k,i,j,m,var;
	Clausula *clausulas = cnf->claus;
	for(k = 1; k <= 9; k++)
		for(i = 1; i <= 9; i++)
			for(j = 1; j <= 9; j++)
				for(m = j + 1; m <= 9; m++) {
					//printf("-%d%d%d -%d%d%d 0\n", i, j, k, i, m, k);
					//printf("l es igual a %d  \n", l);
					var = (i-1)*81+(k-1);
					clausulas[*l].numVariables = 2;
					clausulas[*l].indices = malloc(sizeof(ParOrdenado)*2);
					clausulas[*l].indices[0].pos = var + (j-1)*9;
					clausulas[*l].indices[1].pos = var + (m-1)*9;
					clausulas[*l].indices[1].bool = 0;
					clausulas[*l].indices[1].bool = 0;
					(*l)++;
				}
}

/*
 * Dos casillas distintas en una misma columna no pueden contener el mismo numero
 */
void reglaColumnas(OutPut* cnf, int* l, int* tail) {
	int k,i,j,m,var;
	Clausula *clausulas = cnf->claus;
	for(k = 1; k <= 9; k++)
		for(i = 1; i <= 9; i++)
			for(j = 1; j <= 9; j++)
				for(m = j + 1; m <= 9; m++) {
					//printf("-%d%d%d -%d%d%d 0\n", j, i, k, l, i, k);
					//printf("l es igual a %d\n", l);
					var = (i-1)*9+(k-1);
					clausulas[*l].numVariables = 2;
					clausulas[*l].indices = malloc(sizeof(ParOrdenado)*2);
					clausulas[*l].indices[0].pos = (j-1)*81+var;
					clausulas[*l].indices[1].pos = (m-1)*81+var;
					clausulas[*l].indices[1].bool = 0;
					clausulas[*l].indices[1].bool = 0;
					(*l)++;
				}
}

/*
 * Dos casillas distintas en un mismo cuadrado no pueden contener el mismo numero
 */
void reglaCuadrados(OutPut* cnf, int* l, int* tail) {
	int ci,cj,k,ui,uj,i,j;
	Clausula *clausulas = cnf->claus;
	for(ci = 0; ci < 3; ci++)
		for(cj = 0; cj < 3; cj++)
			for(k = 1; k <= 9; k++) {
				for(ui = 3 * ci + 1; ui <= 3 * ci + 3; ui++)
					for(uj = 3 * cj + 1; uj <= 3 * cj + 3; uj++)
						for(i = 3 * ci + 1; i <= 3 * ci + 3; i++)
							for(j = 3 * cj + 1; j <= 3 * cj + 3; j++)
								if(ui < i || (ui == i && j > uj) )  {
									//printf("l es igual a %d\n", l);
									clausulas[*l].numVariables = 2;
									clausulas[*l].indices = malloc(sizeof(ParOrdenado)*2);
									clausulas[*l].indices[0].pos = (ui-1)*81+(uj-1)*9+(k-1);
									clausulas[*l].indices[1].pos = (i-1)*81+(j-1)*9+(k-1);
									clausulas[*l].indices[1].bool = 0;
									clausulas[*l].indices[1].bool = 0;

									(*l)++;
								}
			}
}
void toCNF(OutPut* cnf) {
	int l=0, tail=0;
	reglaGeneral(cnf,&l,&tail);
	reglaCasillas(cnf,&l,&tail);
	reglaFilas(cnf,&l,&tail);
	reglaColumnas(cnf,&l,&tail);
	reglaCuadrados(cnf,&l,&tail);
}

void valoresIniciales(int** table, OutPut* cnf) {
	int i, j, k;

	for (i = 0; i < 9; i++){
		for (j = 0; j < 9; j++){
			if (table[i][j] != 0) {
				//transformo de tabla 2d a arreglo de variables
				// los valores del sudoku si van de 1 a 9 en vez de 0 a 8 por ello el -1
				k = i * 81 + j * 9 + table[i][j] - 1;

				//printf("%d",k);
				cnf->varias[k].asignacion = 1;
			}
		}
	}
}
